.cent(Thesis Proposal in Program Synthesis)
 
Verification of program correctness, although a laudable goal, has proven to
be more difficult than at first hoped. 
To attempt verification of a program written by someone else is clearly a
monumental task.  It is difficult enough to read someone else's program and
determine what is going on; it is nearly impossible to read the program and
figure out what the programmer had intended to do.  Even when verification
is done by the original programmer, we are asking a lot.  This person must
be able (assuming a structured approach to the task) to move from logical
assumptions about the problem domain (whether or
not these are formalized) to an implementation in language X, and then back
again to the logical base as a source of assertions from which the verification
conditions can be derived.
 
The premise on which this project is based is that verification of an existing
program is an awkward, even backward, way of obtaining a correct program.  
Correctness should be considered in the design and programming stages, not as
an afterthought.
 
 
We intend to take logical knowledge of the
problem domain and automatically synthesize a correct program in the 
required language.  
Good programming style indicates an abstract
approach to the task.  One describes what is to be done in terms of the
(abstract) problem domain, not in terms of some encoding.
 
Similar systems to the one we are proposing have been considered by others.
(Manna & Waldinger, Green et.al. (PSI), Burstall & Darlington, Buchanan, Bauer et. al.)
Buchanan develops programs in an ALGOL-like
language.
Manna and Waldinger synthesize LISP programs; Burstall and Darlington work
with recursion equations.  ...  It seems that all the work done so far has
been concerned with generating programs in a specific language.
  This approach is advantageous in that one is able to use knowledge
of the particular target language and its idiosyncracies to develop efficient
programs.  However, one also loses generality in so restricting the process.
Although it could certainly be done
it is not clear how to extend the synthesis process to other languages,
due to the built in knowledge of the target language.
 
Several people are also working on program transformation systems which
translate a program written in a high level abstract (readable) way
into a more efficient, lower level program in the same language. [Bauer et
al,1977] [Gerhart,1975] [Darlington and Burstall,1976] [Loveman, 1977]
 
From the logic description of the problem
we synthesize an algorithm expressed in an intermediate
language, and then translate this
algorithm into the selected target language.  The process of adding a
new target language to the system is described step by step.  The advantages
of such a system are obvious.  It allows us to specify programs at a very
high level of abstraction where our thinking is not clouded by implementation
issues, and our design is not restricted by availability of particular
constructs.  The assertions we make are more likely to be correct in such
an environment.  (In order to prove correctness we need to go to logic
anyway.)  It is better to go early, in the design of the program, than to work
from an artificially constrained conception of the program.
 
We describe what is required to specify a program for the system.  Logic as a
programming language is discussed, and the restrictions implied by the other
specifications given.  Termination of programs is guaranteed.  The intermediate
language is described in detail and discussed, and the semantics are proved to
be equivalent to that provided by the specifications.  The mapping from input
specifications to intermediate language is presented.  A general plan for
adding target languages to the system is provided, and the implementations
for LISP and PASCAL are discussed.  Several suggestions for further research
projects which presented themselves along the way are offered.